stream.jani:model: info: stream is an MA model.
stream.jani:variables[5]: info: Expanding variable "s" into 4 locations in automaton "streamingclient".
stream.jani: info: Need 8 bytes per state.
stream.jani: info: Explored 1502501 states for N=1000.
stream.jani:properties[0]: warning: Computing minimum expected reward in property "exp_buffertime" without checking for zero-reward end components.
Peak memory usage: 593 MB
Analysis results for stream.jani
Experiment N=1000
+ State space exploration
State size: 8 bytes
States: 1502501
Transitions: 2002001
Branches: 3001001
Rate: 712761 states/s
Time: 2.3 s
+ Property exp_buffertime
Value: 8.91950557292716
Bounds: [8.91950557292716, infinity)
Time: 167.8 s
+ Precomputations
Max. prob. 1 states: 1502501
Time for max. prob. 1 states: 144.3 s
+ Essential states
Iterations: 2
Essential states: 1500502
Transitions: 2000002
Branches: 2999002
Time: 0.4 s
+ Value iteration
Final error: 0
Iterations: 336
Time: 23.1 s
Exported results to file "/out.txt".